pnueli-zuck.5.jani:model: info: pnueli-zuck.5 is an MDP model.
pnueli-zuck.5.jani:variables[0]: info: Expanding variable "p0" into 16 locations in automaton "process0".
pnueli-zuck.5.jani:variables[1]: info: Expanding variable "p1" into 16 locations in automaton "process1".
pnueli-zuck.5.jani:variables[2]: info: Expanding variable "p2" into 16 locations in automaton "process2".
pnueli-zuck.5.jani:variables[3]: info: Expanding variable "p3" into 16 locations in automaton "process3".
pnueli-zuck.5.jani:variables[4]: info: Expanding variable "p4" into 16 locations in automaton "process4".
pnueli-zuck.5.jani: info: Need 16 bytes per state.
FRET called...
Peak memory usage: 49 MB
Analysis results for pnueli-zuck.5.jani
Property live
Probability: 1
Time: 0.0 s